$\forall$$T$:Type$_{\mbox{\scriptsize i}}$, $S$:(($\mathbb{N}\rightarrow$$T$)$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$). generic\{i:l\}($T$; $f$.$S$($f$)) $\in$ Prop$_{\mbox{\scriptsize i'}}$